'Weak Dependency Graph [60.0]' ------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(ok(X)) -> ok(f(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X))} Details: We have computed the following set of weak (innermost) dependency pairs: { active^#(f(0())) -> c_0(cons^#(0(), f(s(0())))) , active^#(f(s(0()))) -> c_1(f^#(p(s(0())))) , active^#(p(s(0()))) -> c_2() , active^#(f(X)) -> c_3(f^#(active(X))) , active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2)) , active^#(s(X)) -> c_5(s^#(active(X))) , active^#(p(X)) -> c_6(p^#(active(X))) , f^#(mark(X)) -> c_7(f^#(X)) , cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2)) , s^#(mark(X)) -> c_9(s^#(X)) , p^#(mark(X)) -> c_10(p^#(X)) , proper^#(f(X)) -> c_11(f^#(proper(X))) , proper^#(0()) -> c_12() , proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2))) , proper^#(s(X)) -> c_14(s^#(proper(X))) , proper^#(p(X)) -> c_15(p^#(proper(X))) , f^#(ok(X)) -> c_16(f^#(X)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2)) , s^#(ok(X)) -> c_18(s^#(X)) , p^#(ok(X)) -> c_19(p^#(X)) , top^#(mark(X)) -> c_20(top^#(proper(X))) , top^#(ok(X)) -> c_21(top^#(active(X)))} The usable rules are: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} The estimated dependency graph contains the following edges: {active^#(f(X)) -> c_3(f^#(active(X)))} ==> {f^#(ok(X)) -> c_16(f^#(X))} {active^#(f(X)) -> c_3(f^#(active(X)))} ==> {f^#(mark(X)) -> c_7(f^#(X))} {active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))} ==> {cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))} {active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))} ==> {cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} {active^#(s(X)) -> c_5(s^#(active(X)))} ==> {s^#(ok(X)) -> c_18(s^#(X))} {active^#(s(X)) -> c_5(s^#(active(X)))} ==> {s^#(mark(X)) -> c_9(s^#(X))} {active^#(p(X)) -> c_6(p^#(active(X)))} ==> {p^#(ok(X)) -> c_19(p^#(X))} {active^#(p(X)) -> c_6(p^#(active(X)))} ==> {p^#(mark(X)) -> c_10(p^#(X))} {f^#(mark(X)) -> c_7(f^#(X))} ==> {f^#(ok(X)) -> c_16(f^#(X))} {f^#(mark(X)) -> c_7(f^#(X))} ==> {f^#(mark(X)) -> c_7(f^#(X))} {cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} ==> {cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))} {cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} ==> {cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} {s^#(mark(X)) -> c_9(s^#(X))} ==> {s^#(ok(X)) -> c_18(s^#(X))} {s^#(mark(X)) -> c_9(s^#(X))} ==> {s^#(mark(X)) -> c_9(s^#(X))} {p^#(mark(X)) -> c_10(p^#(X))} ==> {p^#(ok(X)) -> c_19(p^#(X))} {p^#(mark(X)) -> c_10(p^#(X))} ==> {p^#(mark(X)) -> c_10(p^#(X))} {proper^#(f(X)) -> c_11(f^#(proper(X)))} ==> {f^#(ok(X)) -> c_16(f^#(X))} {proper^#(f(X)) -> c_11(f^#(proper(X)))} ==> {f^#(mark(X)) -> c_7(f^#(X))} {proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))} ==> {cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))} {proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))} ==> {cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} {proper^#(s(X)) -> c_14(s^#(proper(X)))} ==> {s^#(ok(X)) -> c_18(s^#(X))} {proper^#(s(X)) -> c_14(s^#(proper(X)))} ==> {s^#(mark(X)) -> c_9(s^#(X))} {proper^#(p(X)) -> c_15(p^#(proper(X)))} ==> {p^#(ok(X)) -> c_19(p^#(X))} {proper^#(p(X)) -> c_15(p^#(proper(X)))} ==> {p^#(mark(X)) -> c_10(p^#(X))} {f^#(ok(X)) -> c_16(f^#(X))} ==> {f^#(ok(X)) -> c_16(f^#(X))} {f^#(ok(X)) -> c_16(f^#(X))} ==> {f^#(mark(X)) -> c_7(f^#(X))} {cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))} ==> {cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))} {cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))} ==> {cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} {s^#(ok(X)) -> c_18(s^#(X))} ==> {s^#(ok(X)) -> c_18(s^#(X))} {s^#(ok(X)) -> c_18(s^#(X))} ==> {s^#(mark(X)) -> c_9(s^#(X))} {p^#(ok(X)) -> c_19(p^#(X))} ==> {p^#(ok(X)) -> c_19(p^#(X))} {p^#(ok(X)) -> c_19(p^#(X))} ==> {p^#(mark(X)) -> c_10(p^#(X))} {top^#(mark(X)) -> c_20(top^#(proper(X)))} ==> {top^#(ok(X)) -> c_21(top^#(active(X)))} {top^#(mark(X)) -> c_20(top^#(proper(X)))} ==> {top^#(mark(X)) -> c_20(top^#(proper(X)))} {top^#(ok(X)) -> c_21(top^#(active(X)))} ==> {top^#(ok(X)) -> c_21(top^#(active(X)))} {top^#(ok(X)) -> c_21(top^#(active(X)))} ==> {top^#(mark(X)) -> c_20(top^#(proper(X)))} We consider the following path(s): 1) { top^#(mark(X)) -> c_20(top^#(proper(X))) , top^#(ok(X)) -> c_21(top^#(active(X)))} The usable rules for this path are the following: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , top^#(mark(X)) -> c_20(top^#(proper(X))) , top^#(ok(X)) -> c_21(top^#(active(X)))} Details: We apply the weight gap principle, strictly orienting the rules {proper(0()) -> ok(0())} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {proper(0()) -> ok(0())} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [1] x1 + [7] c_20(x1) = [1] x1 + [1] c_21(x1) = [1] x1 + [1] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {top^#(mark(X)) -> c_20(top^#(proper(X)))} and weakly orienting the rules {proper(0()) -> ok(0())} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {top^#(mark(X)) -> c_20(top^#(proper(X)))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [1] x1 + [15] c_20(x1) = [1] x1 + [0] c_21(x1) = [1] x1 + [1] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} and weakly orienting the rules { top^#(mark(X)) -> c_20(top^#(proper(X))) , proper(0()) -> ok(0())} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [1] x1 + [15] c_20(x1) = [1] x1 + [0] c_21(x1) = [1] x1 + [3] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(p(s(0()))) -> mark(0())} and weakly orienting the rules { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , top^#(mark(X)) -> c_20(top^#(proper(X))) , proper(0()) -> ok(0())} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(p(s(0()))) -> mark(0())} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [8] proper(x1) = [1] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [1] x1 + [0] c_20(x1) = [1] x1 + [1] c_21(x1) = [1] x1 + [8] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {top^#(ok(X)) -> c_21(top^#(active(X)))} and weakly orienting the rules { active(p(s(0()))) -> mark(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , top^#(mark(X)) -> c_20(top^#(proper(X))) , proper(0()) -> ok(0())} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {top^#(ok(X)) -> c_21(top^#(active(X)))} Details: Interpretation Functions: active(x1) = [1] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [4] cons(x1, x2) = [1] x1 + [1] x2 + [8] s(x1) = [1] x1 + [8] p(x1) = [1] x1 + [12] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [1] x1 + [3] c_20(x1) = [1] x1 + [1] c_21(x1) = [1] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { top^#(ok(X)) -> c_21(top^#(active(X))) , active(p(s(0()))) -> mark(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , top^#(mark(X)) -> c_20(top^#(proper(X))) , proper(0()) -> ok(0())} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { top^#(ok(X)) -> c_21(top^#(active(X))) , active(p(s(0()))) -> mark(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , top^#(mark(X)) -> c_20(top^#(proper(X))) , proper(0()) -> ok(0())} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { active_0(2) -> 4 , 0_0() -> 2 , mark_0(2) -> 2 , proper_0(2) -> 6 , ok_0(2) -> 2 , ok_0(2) -> 6 , top^#_0(2) -> 1 , top^#_0(4) -> 3 , top^#_0(6) -> 5 , c_20_0(5) -> 1 , c_21_0(3) -> 1 , c_21_0(3) -> 5} 2) { active^#(p(X)) -> c_6(p^#(active(X))) , p^#(ok(X)) -> c_19(p^#(X)) , p^#(mark(X)) -> c_10(p^#(X))} The usable rules for this path are the following: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , active^#(p(X)) -> c_6(p^#(active(X))) , p^#(ok(X)) -> c_19(p^#(X)) , p^#(mark(X)) -> c_10(p^#(X))} Details: We apply the weight gap principle, strictly orienting the rules {p^#(mark(X)) -> c_10(p^#(X))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {p^#(mark(X)) -> c_10(p^#(X))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [1] x1 + [0] p^#(x1) = [1] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [1] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [1] x1 + [1] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active^#(p(X)) -> c_6(p^#(active(X)))} and weakly orienting the rules {p^#(mark(X)) -> c_10(p^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active^#(p(X)) -> c_6(p^#(active(X)))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [9] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [1] x1 + [1] p^#(x1) = [1] x1 + [1] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [1] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [1] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , p^#(ok(X)) -> c_19(p^#(X))} and weakly orienting the rules { active^#(p(X)) -> c_6(p^#(active(X))) , p^#(mark(X)) -> c_10(p^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , p^#(ok(X)) -> c_19(p^#(X))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [9] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [1] x1 + [7] p^#(x1) = [1] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [1] x1 + [1] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [1] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(p(s(0()))) -> mark(0())} and weakly orienting the rules { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , p^#(ok(X)) -> c_19(p^#(X)) , active^#(p(X)) -> c_6(p^#(active(X))) , p^#(mark(X)) -> c_10(p^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(p(s(0()))) -> mark(0())} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [8] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [1] x1 + [2] p^#(x1) = [1] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [1] x1 + [1] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [1] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(f(s(0()))) -> mark(f(p(s(0()))))} and weakly orienting the rules { active(p(s(0()))) -> mark(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , p^#(ok(X)) -> c_19(p^#(X)) , active^#(p(X)) -> c_6(p^#(active(X))) , p^#(mark(X)) -> c_10(p^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(f(s(0()))) -> mark(f(p(s(0()))))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [1] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [13] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [1] x1 + [0] p^#(x1) = [1] x1 + [12] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [1] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [1] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(f(0())) -> mark(cons(0(), f(s(0()))))} and weakly orienting the rules { active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , p^#(ok(X)) -> c_19(p^#(X)) , active^#(p(X)) -> c_6(p^#(active(X))) , p^#(mark(X)) -> c_10(p^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(f(0())) -> mark(cons(0(), f(s(0()))))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [8] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [1] x1 + [0] p^#(x1) = [1] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [1] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [1] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , p^#(ok(X)) -> c_19(p^#(X)) , active^#(p(X)) -> c_6(p^#(active(X))) , p^#(mark(X)) -> c_10(p^#(X))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , p^#(ok(X)) -> c_19(p^#(X)) , active^#(p(X)) -> c_6(p^#(active(X))) , p^#(mark(X)) -> c_10(p^#(X))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , active^#_0(3) -> 11 , active^#_0(4) -> 11 , active^#_0(9) -> 11 , p^#_0(3) -> 22 , p^#_0(4) -> 22 , p^#_0(9) -> 22 , c_10_0(22) -> 22 , c_19_0(22) -> 22} 3) { active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2)) , cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} The usable rules for this path are the following: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2)) , cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} Details: We apply the weight gap principle, strictly orienting the rules { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2)) , cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2)) , cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [9] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [1] x1 + [1] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [1] x1 + [1] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [1] x1 + [1] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))} and weakly orienting the rules { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2)) , cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [5] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [9] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [1] x1 + [1] x2 + [7] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [1] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [1] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(p(s(0()))) -> mark(0())} and weakly orienting the rules { active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2)) , cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(p(s(0()))) -> mark(0())} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [2] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [1] x1 + [1] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [1] x1 + [1] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [1] x1 + [1] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(f(0())) -> mark(cons(0(), f(s(0()))))} and weakly orienting the rules { active(p(s(0()))) -> mark(0()) , active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2)) , cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(f(0())) -> mark(cons(0(), f(s(0()))))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [4] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [5] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [1] x1 + [1] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [1] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [1] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(f(s(0()))) -> mark(f(p(s(0()))))} and weakly orienting the rules { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(p(s(0()))) -> mark(0()) , active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2)) , cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(f(s(0()))) -> mark(f(p(s(0()))))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [1] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [8] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [1] x1 + [1] x2 + [2] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [1] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [1] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { active(f(s(0()))) -> mark(f(p(s(0())))) , active(f(0())) -> mark(cons(0(), f(s(0())))) , active(p(s(0()))) -> mark(0()) , active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2)) , cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { active(f(s(0()))) -> mark(f(p(s(0())))) , active(f(0())) -> mark(cons(0(), f(s(0())))) , active(p(s(0()))) -> mark(0()) , active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2)) , cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , active^#_0(3) -> 11 , active^#_0(4) -> 11 , active^#_0(9) -> 11 , cons^#_0(3, 3) -> 13 , cons^#_0(3, 4) -> 13 , cons^#_0(3, 9) -> 13 , cons^#_0(4, 3) -> 13 , cons^#_0(4, 4) -> 13 , cons^#_0(4, 9) -> 13 , cons^#_0(9, 3) -> 13 , cons^#_0(9, 4) -> 13 , cons^#_0(9, 9) -> 13 , c_8_0(13) -> 13 , c_17_0(13) -> 13} 4) { active^#(s(X)) -> c_5(s^#(active(X))) , s^#(ok(X)) -> c_18(s^#(X)) , s^#(mark(X)) -> c_9(s^#(X))} The usable rules for this path are the following: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , active^#(s(X)) -> c_5(s^#(active(X))) , s^#(ok(X)) -> c_18(s^#(X)) , s^#(mark(X)) -> c_9(s^#(X))} Details: We apply the weight gap principle, strictly orienting the rules {s^#(mark(X)) -> c_9(s^#(X))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {s^#(mark(X)) -> c_9(s^#(X))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [0] s^#(x1) = [1] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [1] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [1] x1 + [1] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active^#(s(X)) -> c_5(s^#(active(X)))} and weakly orienting the rules {s^#(mark(X)) -> c_9(s^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active^#(s(X)) -> c_5(s^#(active(X)))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [9] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [0] s^#(x1) = [1] x1 + [7] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [1] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [1] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , s^#(ok(X)) -> c_18(s^#(X))} and weakly orienting the rules { active^#(s(X)) -> c_5(s^#(active(X))) , s^#(mark(X)) -> c_9(s^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , s^#(ok(X)) -> c_18(s^#(X))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [0] s^#(x1) = [1] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [1] x1 + [1] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [1] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(p(s(0()))) -> mark(0())} and weakly orienting the rules { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , s^#(ok(X)) -> c_18(s^#(X)) , active^#(s(X)) -> c_5(s^#(active(X))) , s^#(mark(X)) -> c_9(s^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(p(s(0()))) -> mark(0())} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [7] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [14] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [0] s^#(x1) = [1] x1 + [13] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [1] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [1] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(f(s(0()))) -> mark(f(p(s(0()))))} and weakly orienting the rules { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(p(s(0()))) -> mark(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , s^#(ok(X)) -> c_18(s^#(X)) , active^#(s(X)) -> c_5(s^#(active(X))) , s^#(mark(X)) -> c_9(s^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(f(s(0()))) -> mark(f(p(s(0()))))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [1] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [15] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [0] s^#(x1) = [1] x1 + [14] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [1] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [1] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { active(f(s(0()))) -> mark(f(p(s(0())))) , active(f(0())) -> mark(cons(0(), f(s(0())))) , active(p(s(0()))) -> mark(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , s^#(ok(X)) -> c_18(s^#(X)) , active^#(s(X)) -> c_5(s^#(active(X))) , s^#(mark(X)) -> c_9(s^#(X))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { active(f(s(0()))) -> mark(f(p(s(0())))) , active(f(0())) -> mark(cons(0(), f(s(0())))) , active(p(s(0()))) -> mark(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , s^#(ok(X)) -> c_18(s^#(X)) , active^#(s(X)) -> c_5(s^#(active(X))) , s^#(mark(X)) -> c_9(s^#(X))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , active^#_0(3) -> 11 , active^#_0(4) -> 11 , active^#_0(9) -> 11 , s^#_0(3) -> 20 , s^#_0(4) -> 20 , s^#_0(9) -> 20 , c_9_0(20) -> 20 , c_18_0(20) -> 20} 5) { active^#(f(X)) -> c_3(f^#(active(X))) , f^#(ok(X)) -> c_16(f^#(X)) , f^#(mark(X)) -> c_7(f^#(X))} The usable rules for this path are the following: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , active^#(f(X)) -> c_3(f^#(active(X))) , f^#(ok(X)) -> c_16(f^#(X)) , f^#(mark(X)) -> c_7(f^#(X))} Details: We apply the weight gap principle, strictly orienting the rules {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [0] c_2() = [0] c_3(x1) = [1] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [1] x1 + [1] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [1] x1 + [1] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {f^#(mark(X)) -> c_7(f^#(X))} and weakly orienting the rules {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {f^#(mark(X)) -> c_7(f^#(X))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [15] c_2() = [0] c_3(x1) = [1] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [1] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [1] x1 + [4] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0())} and weakly orienting the rules { f^#(mark(X)) -> c_7(f^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0())} Details: Interpretation Functions: active(x1) = [1] x1 + [13] f(x1) = [1] x1 + [0] 0() = [4] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [7] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [0] c_2() = [0] c_3(x1) = [1] x1 + [4] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [1] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [1] x1 + [1] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active^#(f(X)) -> c_3(f^#(active(X)))} and weakly orienting the rules { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , f^#(mark(X)) -> c_7(f^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active^#(f(X)) -> c_3(f^#(active(X)))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [3] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [0] c_2() = [0] c_3(x1) = [1] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [1] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [1] x1 + [1] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {f^#(ok(X)) -> c_16(f^#(X))} and weakly orienting the rules { active^#(f(X)) -> c_3(f^#(active(X))) , active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , f^#(mark(X)) -> c_7(f^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {f^#(ok(X)) -> c_16(f^#(X))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [8] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [9] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [1] c_2() = [0] c_3(x1) = [1] x1 + [7] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [1] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [1] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { f^#(ok(X)) -> c_16(f^#(X)) , active^#(f(X)) -> c_3(f^#(active(X))) , active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , f^#(mark(X)) -> c_7(f^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { f^#(ok(X)) -> c_16(f^#(X)) , active^#(f(X)) -> c_3(f^#(active(X))) , active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , f^#(mark(X)) -> c_7(f^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , active^#_0(3) -> 11 , active^#_0(4) -> 11 , active^#_0(9) -> 11 , f^#_0(3) -> 15 , f^#_0(4) -> 15 , f^#_0(9) -> 15 , c_7_0(15) -> 15 , c_16_0(15) -> 15} 6) {active^#(f(X)) -> c_3(f^#(active(X)))} The usable rules for this path are the following: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , active^#(f(X)) -> c_3(f^#(active(X)))} Details: We apply the weight gap principle, strictly orienting the rules {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [0] c_2() = [0] c_3(x1) = [1] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active^#(f(X)) -> c_3(f^#(active(X)))} and weakly orienting the rules {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active^#(f(X)) -> c_3(f^#(active(X)))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [8] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [9] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [0] c_2() = [0] c_3(x1) = [1] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(p(s(0()))) -> mark(0())} and weakly orienting the rules { active^#(f(X)) -> c_3(f^#(active(X))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(p(s(0()))) -> mark(0())} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [8] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [9] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [0] c_2() = [0] c_3(x1) = [1] x1 + [4] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(f(s(0()))) -> mark(f(p(s(0()))))} and weakly orienting the rules { active(p(s(0()))) -> mark(0()) , active^#(f(X)) -> c_3(f^#(active(X))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(f(s(0()))) -> mark(f(p(s(0()))))} Details: Interpretation Functions: active(x1) = [1] x1 + [7] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [7] s(x1) = [1] x1 + [1] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [11] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [1] c_2() = [0] c_3(x1) = [1] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(f(0())) -> mark(cons(0(), f(s(0()))))} and weakly orienting the rules { active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active^#(f(X)) -> c_3(f^#(active(X))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(f(0())) -> mark(cons(0(), f(s(0()))))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [9] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [4] c_2() = [0] c_3(x1) = [1] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active^#(f(X)) -> c_3(f^#(active(X))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active^#(f(X)) -> c_3(f^#(active(X))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , active^#_0(3) -> 11 , active^#_0(4) -> 11 , active^#_0(9) -> 11 , f^#_0(3) -> 15 , f^#_0(4) -> 15 , f^#_0(9) -> 15} 7) {active^#(p(X)) -> c_6(p^#(active(X)))} The usable rules for this path are the following: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , active^#(p(X)) -> c_6(p^#(active(X)))} Details: We apply the weight gap principle, strictly orienting the rules {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [1] x1 + [0] p^#(x1) = [1] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active^#(p(X)) -> c_6(p^#(active(X)))} and weakly orienting the rules {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active^#(p(X)) -> c_6(p^#(active(X)))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [8] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [9] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [1] x1 + [0] p^#(x1) = [1] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(p(s(0()))) -> mark(0())} and weakly orienting the rules { active^#(p(X)) -> c_6(p^#(active(X))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(p(s(0()))) -> mark(0())} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [8] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [1] x1 + [0] p^#(x1) = [1] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(f(s(0()))) -> mark(f(p(s(0()))))} and weakly orienting the rules { active(p(s(0()))) -> mark(0()) , active^#(p(X)) -> c_6(p^#(active(X))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(f(s(0()))) -> mark(f(p(s(0()))))} Details: Interpretation Functions: active(x1) = [1] x1 + [3] f(x1) = [1] x1 + [0] 0() = [2] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [3] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [5] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [1] x1 + [0] p^#(x1) = [1] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(f(0())) -> mark(cons(0(), f(s(0()))))} and weakly orienting the rules { active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active^#(p(X)) -> c_6(p^#(active(X))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(f(0())) -> mark(cons(0(), f(s(0()))))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [9] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [1] x1 + [0] p^#(x1) = [1] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active^#(p(X)) -> c_6(p^#(active(X))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active^#(p(X)) -> c_6(p^#(active(X))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , active^#_0(3) -> 11 , active^#_0(4) -> 11 , active^#_0(9) -> 11 , p^#_0(3) -> 22 , p^#_0(4) -> 22 , p^#_0(9) -> 22} 8) {active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))} The usable rules for this path are the following: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))} Details: We apply the weight gap principle, strictly orienting the rules {active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [9] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [1] x1 + [1] x2 + [2] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} and weakly orienting the rules {active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [8] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [1] x1 + [1] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(p(s(0()))) -> mark(0())} and weakly orienting the rules { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(p(s(0()))) -> mark(0())} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [8] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [1] x1 + [1] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(f(s(0()))) -> mark(f(p(s(0()))))} and weakly orienting the rules { active(p(s(0()))) -> mark(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(f(s(0()))) -> mark(f(p(s(0()))))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [1] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [9] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [1] x1 + [1] x2 + [3] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [1] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(f(0())) -> mark(cons(0(), f(s(0()))))} and weakly orienting the rules { active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(f(0())) -> mark(cons(0(), f(s(0()))))} Details: Interpretation Functions: active(x1) = [1] x1 + [12] f(x1) = [1] x1 + [0] 0() = [8] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [12] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [1] x1 + [1] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [1] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , active^#_0(3) -> 11 , active^#_0(4) -> 11 , active^#_0(9) -> 11 , cons^#_0(3, 3) -> 13 , cons^#_0(3, 4) -> 13 , cons^#_0(3, 9) -> 13 , cons^#_0(4, 3) -> 13 , cons^#_0(4, 4) -> 13 , cons^#_0(4, 9) -> 13 , cons^#_0(9, 3) -> 13 , cons^#_0(9, 4) -> 13 , cons^#_0(9, 9) -> 13} 9) {active^#(s(X)) -> c_5(s^#(active(X)))} The usable rules for this path are the following: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , active^#(s(X)) -> c_5(s^#(active(X)))} Details: We apply the weight gap principle, strictly orienting the rules {active^#(s(X)) -> c_5(s^#(active(X)))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active^#(s(X)) -> c_5(s^#(active(X)))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [9] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [0] s^#(x1) = [1] x1 + [2] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} and weakly orienting the rules {active^#(s(X)) -> c_5(s^#(active(X)))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [8] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [0] s^#(x1) = [1] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {active(p(s(0()))) -> mark(0())} and weakly orienting the rules { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , active^#(s(X)) -> c_5(s^#(active(X)))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active(p(s(0()))) -> mark(0())} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [1] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [8] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [8] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [0] s^#(x1) = [1] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0()))))} and weakly orienting the rules { active(p(s(0()))) -> mark(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , active^#(s(X)) -> c_5(s^#(active(X)))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0()))))} Details: Interpretation Functions: active(x1) = [1] x1 + [1] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [5] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [1] x1 + [4] s^#(x1) = [1] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , active^#(s(X)) -> c_5(s^#(active(X)))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { active(f(X)) -> f(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(p(X)) -> p(active(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { active(f(0())) -> mark(cons(0(), f(s(0())))) , active(f(s(0()))) -> mark(f(p(s(0())))) , active(p(s(0()))) -> mark(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , active^#(s(X)) -> c_5(s^#(active(X)))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , active^#_0(3) -> 11 , active^#_0(4) -> 11 , active^#_0(9) -> 11 , s^#_0(3) -> 20 , s^#_0(4) -> 20 , s^#_0(9) -> 20} 10) { proper^#(p(X)) -> c_15(p^#(proper(X))) , p^#(ok(X)) -> c_19(p^#(X)) , p^#(mark(X)) -> c_10(p^#(X))} The usable rules for this path are the following: { proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(p(X)) -> c_15(p^#(proper(X))) , p^#(ok(X)) -> c_19(p^#(X)) , p^#(mark(X)) -> c_10(p^#(X))} Details: We apply the weight gap principle, strictly orienting the rules {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [1] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [1] x1 + [1] proper^#(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [1] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [1] x1 + [1] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {p^#(ok(X)) -> c_19(p^#(X))} and weakly orienting the rules {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {p^#(ok(X)) -> c_19(p^#(X))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [1] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [1] x1 + [1] proper^#(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [1] x1 + [1] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [1] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {p^#(mark(X)) -> c_10(p^#(X))} and weakly orienting the rules { p^#(ok(X)) -> c_19(p^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {p^#(mark(X)) -> c_10(p^#(X))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [2] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [1] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [1] x1 + [1] proper^#(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [1] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [1] x1 + [1] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {proper^#(p(X)) -> c_15(p^#(proper(X)))} and weakly orienting the rules { p^#(mark(X)) -> c_10(p^#(X)) , p^#(ok(X)) -> c_19(p^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {proper^#(p(X)) -> c_15(p^#(proper(X)))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [1] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [1] x1 + [0] proper^#(x1) = [1] x1 + [9] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [1] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [1] x1 + [1] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {proper(0()) -> ok(0())} and weakly orienting the rules { proper^#(p(X)) -> c_15(p^#(proper(X))) , p^#(mark(X)) -> c_10(p^#(X)) , p^#(ok(X)) -> c_19(p^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {proper(0()) -> ok(0())} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [8] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [1] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [1] x1 + [0] proper^#(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [1] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [1] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { proper(0()) -> ok(0()) , proper^#(p(X)) -> c_15(p^#(proper(X))) , p^#(mark(X)) -> c_10(p^#(X)) , p^#(ok(X)) -> c_19(p^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { proper(0()) -> ok(0()) , proper^#(p(X)) -> c_15(p^#(proper(X))) , p^#(mark(X)) -> c_10(p^#(X)) , p^#(ok(X)) -> c_19(p^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , p^#_0(3) -> 22 , p^#_0(4) -> 22 , p^#_0(9) -> 22 , c_10_0(22) -> 22 , proper^#_0(3) -> 27 , proper^#_0(4) -> 27 , proper^#_0(9) -> 27 , c_19_0(22) -> 22} 11) { proper^#(s(X)) -> c_14(s^#(proper(X))) , s^#(ok(X)) -> c_18(s^#(X)) , s^#(mark(X)) -> c_9(s^#(X))} The usable rules for this path are the following: { proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(s(X)) -> c_14(s^#(proper(X))) , s^#(ok(X)) -> c_18(s^#(X)) , s^#(mark(X)) -> c_9(s^#(X))} Details: We apply the weight gap principle, strictly orienting the rules {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [1] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [1] x1 + [1] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [1] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [1] x1 + [1] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {s^#(ok(X)) -> c_18(s^#(X))} and weakly orienting the rules {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {s^#(ok(X)) -> c_18(s^#(X))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [1] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [1] x1 + [1] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [1] x1 + [2] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [1] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {s^#(mark(X)) -> c_9(s^#(X))} and weakly orienting the rules { s^#(ok(X)) -> c_18(s^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {s^#(mark(X)) -> c_9(s^#(X))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [2] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [1] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [1] x1 + [1] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [1] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [1] x1 + [1] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {proper^#(s(X)) -> c_14(s^#(proper(X)))} and weakly orienting the rules { s^#(mark(X)) -> c_9(s^#(X)) , s^#(ok(X)) -> c_18(s^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {proper^#(s(X)) -> c_14(s^#(proper(X)))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [1] x1 + [1] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [1] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [9] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [1] x1 + [1] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [1] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {proper(0()) -> ok(0())} and weakly orienting the rules { proper^#(s(X)) -> c_14(s^#(proper(X))) , s^#(mark(X)) -> c_9(s^#(X)) , s^#(ok(X)) -> c_18(s^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {proper(0()) -> ok(0())} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [5] ok(x1) = [1] x1 + [4] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [1] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [1] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [5] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [1] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [1] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { proper(0()) -> ok(0()) , proper^#(s(X)) -> c_14(s^#(proper(X))) , s^#(mark(X)) -> c_9(s^#(X)) , s^#(ok(X)) -> c_18(s^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { proper(0()) -> ok(0()) , proper^#(s(X)) -> c_14(s^#(proper(X))) , s^#(mark(X)) -> c_9(s^#(X)) , s^#(ok(X)) -> c_18(s^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , s^#_0(3) -> 20 , s^#_0(4) -> 20 , s^#_0(9) -> 20 , c_9_0(20) -> 20 , proper^#_0(3) -> 27 , proper^#_0(4) -> 27 , proper^#_0(9) -> 27 , c_18_0(20) -> 20} 12) { proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2))) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2)) , cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} The usable rules for this path are the following: { proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2))) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2)) , cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} Details: We apply the weight gap principle, strictly orienting the rules { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [1] x1 + [1] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [1] x1 + [1] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [1] x1 + [1] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [1] x1 + [1] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))} and weakly orienting the rules { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [1] x1 + [1] x2 + [2] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [1] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [8] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [1] x1 + [3] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [1] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {proper(0()) -> ok(0())} and weakly orienting the rules { proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {proper(0()) -> ok(0())} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [1] x1 + [1] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [1] x1 + [9] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [4] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [1] x1 + [2] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [1] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} and weakly orienting the rules { proper(0()) -> ok(0()) , proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [4] mark(x1) = [1] x1 + [8] cons(x1, x2) = [1] x1 + [1] x2 + [8] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [4] proper(x1) = [1] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [1] x1 + [1] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [1] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [8] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [1] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [1] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2)) , proper(0()) -> ok(0()) , proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2)) , proper(0()) -> ok(0()) , proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , cons^#_0(3, 3) -> 13 , cons^#_0(3, 4) -> 13 , cons^#_0(3, 9) -> 13 , cons^#_0(4, 3) -> 13 , cons^#_0(4, 4) -> 13 , cons^#_0(4, 9) -> 13 , cons^#_0(9, 3) -> 13 , cons^#_0(9, 4) -> 13 , cons^#_0(9, 9) -> 13 , c_8_0(13) -> 13 , proper^#_0(3) -> 27 , proper^#_0(4) -> 27 , proper^#_0(9) -> 27 , c_17_0(13) -> 13} 13) { proper^#(f(X)) -> c_11(f^#(proper(X))) , f^#(ok(X)) -> c_16(f^#(X)) , f^#(mark(X)) -> c_7(f^#(X))} The usable rules for this path are the following: { proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(f(X)) -> c_11(f^#(proper(X))) , f^#(ok(X)) -> c_16(f^#(X)) , f^#(mark(X)) -> c_7(f^#(X))} Details: We apply the weight gap principle, strictly orienting the rules { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , f^#(ok(X)) -> c_16(f^#(X))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , f^#(ok(X)) -> c_16(f^#(X))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [4] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [3] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [1] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [1] c_11(x1) = [1] x1 + [1] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [1] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {f^#(mark(X)) -> c_7(f^#(X))} and weakly orienting the rules { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , f^#(ok(X)) -> c_16(f^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {f^#(mark(X)) -> c_7(f^#(X))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [2] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [1] x1 + [1] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [1] c_11(x1) = [1] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [1] x1 + [1] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {proper^#(f(X)) -> c_11(f^#(proper(X)))} and weakly orienting the rules { f^#(mark(X)) -> c_7(f^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , f^#(ok(X)) -> c_16(f^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {proper^#(f(X)) -> c_11(f^#(proper(X)))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [1] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [1] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [9] c_11(x1) = [1] x1 + [1] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [1] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {proper(0()) -> ok(0())} and weakly orienting the rules { proper^#(f(X)) -> c_11(f^#(proper(X))) , f^#(mark(X)) -> c_7(f^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , f^#(ok(X)) -> c_16(f^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {proper(0()) -> ok(0())} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [4] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [1] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [1] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [5] c_11(x1) = [1] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [1] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { proper(0()) -> ok(0()) , proper^#(f(X)) -> c_11(f^#(proper(X))) , f^#(mark(X)) -> c_7(f^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , f^#(ok(X)) -> c_16(f^#(X))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { proper(0()) -> ok(0()) , proper^#(f(X)) -> c_11(f^#(proper(X))) , f^#(mark(X)) -> c_7(f^#(X)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , f^#(ok(X)) -> c_16(f^#(X))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , f^#_0(3) -> 15 , f^#_0(4) -> 15 , f^#_0(9) -> 15 , c_7_0(15) -> 15 , proper^#_0(3) -> 27 , proper^#_0(4) -> 27 , proper^#_0(9) -> 27 , c_16_0(15) -> 15} 14) {proper^#(p(X)) -> c_15(p^#(proper(X)))} The usable rules for this path are the following: { proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(p(X)) -> c_15(p^#(proper(X)))} Details: We apply the weight gap principle, strictly orienting the rules {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [8] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [1] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [1] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [1] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {proper^#(p(X)) -> c_15(p^#(proper(X)))} and weakly orienting the rules {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {proper^#(p(X)) -> c_15(p^#(proper(X)))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [4] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [1] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [9] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [1] x1 + [2] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {proper(0()) -> ok(0())} and weakly orienting the rules { proper^#(p(X)) -> c_15(p^#(proper(X))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {proper(0()) -> ok(0())} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [15] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [8] s(x1) = [1] x1 + [4] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [1] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [8] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [1] x1 + [1] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { proper(0()) -> ok(0()) , proper^#(p(X)) -> c_15(p^#(proper(X))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { proper(0()) -> ok(0()) , proper^#(p(X)) -> c_15(p^#(proper(X))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , p^#_0(3) -> 22 , p^#_0(4) -> 22 , p^#_0(9) -> 22 , proper^#_0(3) -> 27 , proper^#_0(4) -> 27 , proper^#_0(9) -> 27} 15) {proper^#(f(X)) -> c_11(f^#(proper(X)))} The usable rules for this path are the following: { proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(f(X)) -> c_11(f^#(proper(X)))} Details: We apply the weight gap principle, strictly orienting the rules {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [8] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [1] c_11(x1) = [1] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {proper^#(f(X)) -> c_11(f^#(proper(X)))} and weakly orienting the rules {cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {proper^#(f(X)) -> c_11(f^#(proper(X)))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [4] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [3] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [9] c_11(x1) = [1] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {proper(0()) -> ok(0())} and weakly orienting the rules { proper^#(f(X)) -> c_11(f^#(proper(X))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {proper(0()) -> ok(0())} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [4] 0() = [3] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [4] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [8] c_11(x1) = [1] x1 + [1] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { proper(0()) -> ok(0()) , proper^#(f(X)) -> c_11(f^#(proper(X))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { proper(0()) -> ok(0()) , proper^#(f(X)) -> c_11(f^#(proper(X))) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , f^#_0(3) -> 15 , f^#_0(4) -> 15 , f^#_0(9) -> 15 , proper^#_0(3) -> 27 , proper^#_0(4) -> 27 , proper^#_0(9) -> 27} 16) {proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))} The usable rules for this path are the following: { proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))} Details: We apply the weight gap principle, strictly orienting the rules { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [1] x1 + [1] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [9] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [1] x1 + [1] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {proper(0()) -> ok(0())} and weakly orienting the rules { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {proper(0()) -> ok(0())} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [5] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [1] x1 + [1] x2 + [3] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [13] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [1] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { proper(0()) -> ok(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { proper(0()) -> ok(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , cons^#_0(3, 3) -> 13 , cons^#_0(3, 4) -> 13 , cons^#_0(3, 9) -> 13 , cons^#_0(4, 3) -> 13 , cons^#_0(4, 4) -> 13 , cons^#_0(4, 9) -> 13 , cons^#_0(9, 3) -> 13 , cons^#_0(9, 4) -> 13 , cons^#_0(9, 9) -> 13 , proper^#_0(3) -> 27 , proper^#_0(4) -> 27 , proper^#_0(9) -> 27} 17) {proper^#(s(X)) -> c_14(s^#(proper(X)))} The usable rules for this path are the following: { proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { proper(f(X)) -> f(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(s(X)) -> c_14(s^#(proper(X)))} Details: We apply the weight gap principle, strictly orienting the rules { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(s(X)) -> c_14(s^#(proper(X)))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(s(X)) -> c_14(s^#(proper(X)))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [8] cons(x1, x2) = [1] x1 + [1] x2 + [0] s(x1) = [1] x1 + [1] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [1] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [1] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [4] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [1] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {proper(0()) -> ok(0())} and weakly orienting the rules { cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(s(X)) -> c_14(s^#(proper(X)))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {proper(0()) -> ok(0())} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [1] x1 + [1] x2 + [4] s(x1) = [1] x1 + [8] p(x1) = [1] x1 + [0] proper(x1) = [1] x1 + [1] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [1] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [1] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { proper(0()) -> ok(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(s(X)) -> c_14(s^#(proper(X)))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { proper(f(X)) -> f(proper(X)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(p(X)) -> p(proper(X)) , f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2))} Weak Rules: { proper(0()) -> ok(0()) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , proper^#(s(X)) -> c_14(s^#(proper(X)))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , s^#_0(3) -> 20 , s^#_0(4) -> 20 , s^#_0(9) -> 20 , proper^#_0(3) -> 27 , proper^#_0(4) -> 27 , proper^#_0(9) -> 27} 18) {active^#(f(s(0()))) -> c_1(f^#(p(s(0()))))} The usable rules for this path are the following: { s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X)) , active^#(f(s(0()))) -> c_1(f^#(p(s(0()))))} Details: We apply the weight gap principle, strictly orienting the rules {active^#(f(s(0()))) -> c_1(f^#(p(s(0()))))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active^#(f(s(0()))) -> c_1(f^#(p(s(0()))))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] 0() = [0] mark(x1) = [1] x1 + [0] cons(x1, x2) = [0] x1 + [0] x2 + [0] s(x1) = [1] x1 + [1] p(x1) = [1] x1 + [1] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [8] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [1] x1 + [1] f^#(x1) = [1] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X))} Weak Rules: {active^#(f(s(0()))) -> c_1(f^#(p(s(0()))))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { s(mark(X)) -> mark(s(X)) , p(mark(X)) -> mark(p(X)) , s(ok(X)) -> ok(s(X)) , p(ok(X)) -> ok(p(X))} Weak Rules: {active^#(f(s(0()))) -> c_1(f^#(p(s(0()))))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , active^#_0(3) -> 11 , active^#_0(4) -> 11 , active^#_0(9) -> 11 , f^#_0(3) -> 15 , f^#_0(4) -> 15 , f^#_0(9) -> 15} 19) {active^#(f(0())) -> c_0(cons^#(0(), f(s(0()))))} The usable rules for this path are the following: { f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X)) , active^#(f(0())) -> c_0(cons^#(0(), f(s(0()))))} Details: We apply the weight gap principle, strictly orienting the rules {active^#(f(0())) -> c_0(cons^#(0(), f(s(0()))))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active^#(f(0())) -> c_0(cons^#(0(), f(s(0()))))} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [1] x1 + [1] 0() = [2] mark(x1) = [1] x1 + [0] cons(x1, x2) = [0] x1 + [0] x2 + [0] s(x1) = [1] x1 + [1] p(x1) = [0] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [1] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [4] c_0(x1) = [1] x1 + [0] cons^#(x1, x2) = [1] x1 + [1] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X))} Weak Rules: {active^#(f(0())) -> c_0(cons^#(0(), f(s(0()))))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { f(mark(X)) -> mark(f(X)) , s(mark(X)) -> mark(s(X)) , f(ok(X)) -> ok(f(X)) , s(ok(X)) -> ok(s(X))} Weak Rules: {active^#(f(0())) -> c_0(cons^#(0(), f(s(0()))))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { 0_0() -> 3 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(9) -> 4 , ok_0(3) -> 9 , ok_0(4) -> 9 , ok_0(9) -> 9 , active^#_0(3) -> 11 , active^#_0(4) -> 11 , active^#_0(9) -> 11 , cons^#_0(3, 3) -> 13 , cons^#_0(3, 4) -> 13 , cons^#_0(3, 9) -> 13 , cons^#_0(4, 3) -> 13 , cons^#_0(4, 4) -> 13 , cons^#_0(4, 9) -> 13 , cons^#_0(9, 3) -> 13 , cons^#_0(9, 4) -> 13 , cons^#_0(9, 9) -> 13} 20) {active^#(p(s(0()))) -> c_2()} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] 0() = [0] mark(x1) = [0] x1 + [0] cons(x1, x2) = [0] x1 + [0] x2 + [0] s(x1) = [0] x1 + [0] p(x1) = [0] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [0] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {active^#(p(s(0()))) -> c_2()} Weak Rules: {} Details: We apply the weight gap principle, strictly orienting the rules {active^#(p(s(0()))) -> c_2()} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {active^#(p(s(0()))) -> c_2()} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] 0() = [0] mark(x1) = [0] x1 + [0] cons(x1, x2) = [0] x1 + [0] x2 + [0] s(x1) = [1] x1 + [0] p(x1) = [1] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [0] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: {active^#(p(s(0()))) -> c_2()} Details: The given problem does not contain any strict rules 21) {proper^#(0()) -> c_12()} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] 0() = [0] mark(x1) = [0] x1 + [0] cons(x1, x2) = [0] x1 + [0] x2 + [0] s(x1) = [0] x1 + [0] p(x1) = [0] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [0] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [0] x1 + [0] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {proper^#(0()) -> c_12()} Weak Rules: {} Details: We apply the weight gap principle, strictly orienting the rules {proper^#(0()) -> c_12()} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {proper^#(0()) -> c_12()} Details: Interpretation Functions: active(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] 0() = [0] mark(x1) = [0] x1 + [0] cons(x1, x2) = [0] x1 + [0] x2 + [0] s(x1) = [0] x1 + [0] p(x1) = [0] x1 + [0] proper(x1) = [0] x1 + [0] ok(x1) = [0] x1 + [0] top(x1) = [0] x1 + [0] active^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] cons^#(x1, x2) = [0] x1 + [0] x2 + [0] c_1(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4(x1) = [0] x1 + [0] c_5(x1) = [0] x1 + [0] s^#(x1) = [0] x1 + [0] c_6(x1) = [0] x1 + [0] p^#(x1) = [0] x1 + [0] c_7(x1) = [0] x1 + [0] c_8(x1) = [0] x1 + [0] c_9(x1) = [0] x1 + [0] c_10(x1) = [0] x1 + [0] proper^#(x1) = [1] x1 + [1] c_11(x1) = [0] x1 + [0] c_12() = [0] c_13(x1) = [0] x1 + [0] c_14(x1) = [0] x1 + [0] c_15(x1) = [0] x1 + [0] c_16(x1) = [0] x1 + [0] c_17(x1) = [0] x1 + [0] c_18(x1) = [0] x1 + [0] c_19(x1) = [0] x1 + [0] top^#(x1) = [0] x1 + [0] c_20(x1) = [0] x1 + [0] c_21(x1) = [0] x1 + [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: {proper^#(0()) -> c_12()} Details: The given problem does not contain any strict rules